<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Maths in Lean : the natural numbers</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="maths-in-lean--the-naturalnumbers" class="markdown-heading">Maths in Lean : the natural numbers <a class="hover-link" href="#maths-in-lean--the-naturalnumbers">#</a></h1>
<p>The natural numbers begin with zero as is standard in computer
science. You can call them <code>nat</code> or <code>ℕ</code> (you get the latter
symbol by typing <code>\N</code> in VS Code).</p>
<p>The naturals are what is called an inductive type, with two
constructors. The first is <code>nat.zero</code>, usually written <code>0</code> or <code>(0:ℕ)</code> in
practice, which is zero. The other constructor is <code>nat.succ</code>, which
takes a natural as input and outputs the next one.</p>
<p>Addition and multiplication are defined by recursion on the second
variable and many proofs of basic stuff in the core library are by
induction on the second variable. The notations <code>+,-,*</code> are shorthand
for the functions <code>nat.add</code>, <code>nat.sub</code> and <code>nat.mul</code> and other notations
(≤, &lt;, |) mean the usual things (get the &quot;divides&quot; symbol with <code>\|</code>.
The <code>%</code> symbol denotes modulus (remainder after division).</p>
<p>Here are some of core Lean's functions for working with <code>nat</code>.</p>
<pre><code class="language-lean">open nat

example : nat.succ (nat.succ 4) = 6 := rfl

example : 4 - 3 = 1 := rfl

example : 5 - 6 = 0 := rfl -- these are naturals

example : 1 ≠ 0 := one_ne_zero

example : 7 * 4 = 28 := rfl

example (m n p : ℕ) : m + p = n + p → m = n := add_right_cancel

example (a b c : ℕ) : a * (b + c) = a * b + a * c := left_distrib a b c

example (m n : ℕ) : succ m ≤ succ n → m ≤ n := le_of_succ_le_succ

example (a b: ℕ) : a &lt; b → ∀ n, 0 &lt; n → a ^ n &lt; b ^ n := pow_lt_pow_of_lt_left
</code></pre>
<p>In mathlib there are more basic functions on the naturals, for example
factorials, lowest common multiples, primes, square roots, and some
modular arithmetic.</p>
<pre><code class="language-lean">import data.nat.dist -- distance function
import data.nat.gcd -- gcd
import data.nat.modeq -- modular arithmetic
import data.nat.prime -- prime number stuff
import data.nat.sqrt  -- square roots
import tactic.norm_num -- a tactic for fast computations

open nat

example : fact 4 = 24 := rfl -- factorial

example (a : ℕ) : fact a &gt; 0 := fact_pos a

example : dist 6 4 = 2 := rfl -- distance function

example (a b : ℕ) : a ≠ b → dist a b &gt; 0 := dist_pos_of_ne

example (a b : ℕ) : gcd a b ∣ a ∧ gcd a b ∣ b := gcd_dvd a b

example : lcm 6 4 = 12 := rfl

example (a b : ℕ) : lcm a b = lcm b a := lcm_comm a b
example (a b : ℕ) : gcd a b * lcm a b = a * b := gcd_mul_lcm a b

example (a b : ℕ) : (∀ k : ℕ, k &gt; 1 → k ∣ a → ¬ (k ∣ b) ) → coprime a b := coprime_of_dvd

-- type the congruence symbol with \==

example : 5 ≡ 8 [MOD 3] := rfl

example (a b c d m : ℕ) : a ≡ b [MOD m] → c ≡ d [MOD m] → a * c ≡ b * d [MOD m] := modeq.modeq_mul

-- nat.sqrt is integer square root (it rounds down).

#eval sqrt 1000047
-- returns 1000

example (a : ℕ) : sqrt (a * a) = a := sqrt_eq a

example (a b : ℕ) : sqrt a &lt; b ↔ a &lt; b * b := sqrt_lt

-- nat.prime n returns whether n is prime or not.
-- We can prove 59 is prime if we first tell Lean that primality
-- is decidable. But it&#x27;s slow because the algorithms are
-- not optimised for the kernel.

instance : decidable (prime 59) := decidable_prime_1 59
example : prime 59 := dec_trivial

-- (The default instance is `nat.decidable_prime`, which can&#x27;t be
-- used by `dec_trivial`, because the kernel would need to unfold
-- irreducible proofs generated by well-founded recursion.)

-- The tactic `norm_num`, amongst other things, provides faster primality testing.

example : prime 104729 := by norm_num

example (p : ℕ) : prime p → p ≥ 2 := prime.two_le

example (p : ℕ) : prime p ↔ p ≥ 2 ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬ (m ∣ p) := prime_def_le_sqrt

example (p : ℕ) : prime p → (∀ m, coprime p m ∨ p ∣ m) := coprime_or_dvd_of_prime

example : ∀ n, ∃ p, p ≥ n ∧ prime p := exists_infinite_primes

-- min_fac returns the smallest prime factor of n (or junk if it doesn&#x27;t have one)

example : min_fac 12 = 2 := rfl

-- `factors n` is the prime factorization of `n`, listed in increasing order.
-- This doesn&#x27;t seem to reduce, and apparently there has not been
-- an attempt to get the kernel to evaluate it sensibly.
-- But we can evaluate it in the virtual machine using #eval .

#eval factors (2^32+1)
-- [641, 6700417]
</code></pre>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/theories/naturals.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>